Inference at * 2 2 1 
Iof proof for Lemma member nth tl:

.....truecase..... NILNIL

1. T : Type
2. n : 
3. 0 < n
4. x:T, L:(T List). (x  nth_tl(n - 1;L))  (x  L)
5. x : T
6. T List
7. u : T
8. v : T List
9. (x  nth_tl(n;v))  (x  v)
10. n  0
  (x  [u / v])  (x  [u / v]) 

latex

 by Auto' 

latex

 .

Definitions	nth_tl(n;as), n - m, #$n, A  B, P  Q, a < b, , Type, (x  l), [car / cdr], x:A. B(x), x:AB(x), s = t, A List, type List, t  T
Lemmas	l member wf